『Homotopy Type Theory: Univalent Foundations of Mathematics』Chapter 1 Type theory

P17～P58

table:訳

witness 証拠？

membership メンバーシップ、所属性？

disprove 反証を挙げる

judgment 判断

propositionally equal 命題として等しい

judgmental equality 判断的等号？、判断としての等しさ？、判断的等質性？

definitional equality 定義的等号？、定義としての等しさ？、定義的等質性？

naive set theory 素朴集合論

assumption 仮定

hypothesis

A has proof

a : A 項aは型Aを持つ

aはAの点である(ホモトピー型理論)

judgmental equality or definitional equality

$ a \equiv b : A または$ a \equiv b

定義により等しい(equal by definition)

propositional equality

$ p : x = y

参考